(VAR X Y) (STRATEGY CONTEXTSENSITIVE (nats) (adx 1) (zeros) (cons) (0) (incr 1) (s) (hd 1) (tl 1) ) (RULES nats -> adx(zeros) zeros -> cons(0,zeros) incr(cons(X,Y)) -> cons(s(X),incr(Y)) adx(cons(X,Y)) -> incr(cons(X,adx(Y))) hd(cons(X,Y)) -> X tl(cons(X,Y)) -> Y )